ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da), m:.
ecl-act(ds; da; m; x)  (event-info(ds;da) List)prop{i:l} 

latex

Definitions	x. t(x), x,y,z. t(x;y;z), A, A  B, x,y,z,w. t(x;y;z;w), x,y. t(x;y), P  Q, P  Q, x:A. B(x), P  Q, False, ecl-act(ds; da; m; x), prop{i:l}, t  T, , x:A. B(x), x(s), x(s1,s2,s3), x(s1,s2,s3,s4), x(s1,s2), subtype(S; T)
Lemmas	Id wf, Knd wf, fpf wf, ecl wf, eq int wf, ifthenelse wf, star-append wf, nat wf, nat plus inc, iseg wf, nat plus wf, le wf, ecl-halt wf, append wf, bool wf, ma-valtype wf, decl-state wf, false wf, event-info wf, ecl ind wf